Iof proof for Lemma fast-fib:
1.
n, a, b:
.
1. {m:
|
1. {
k:. (a = fib(k)) 
((k 
0) (b = 0)) ((0 < k) (b = fib(k - 1))) (m = fib(n+k))}
n:. {m:| m = fib(n)}
by RenameVar `f' 1
1:
1: 1. n, a, b:.
1: 1. {m:|
1: 1. {k:.
1: 1. {(a = fib(k)) ((k 0) (b = 0)) ((0 < k) (b = fib(k - 1))) (m = fib(n+k))}
1: n:. {m:| m = fib(n)}
.